perm filename KNOW.NOT[226,JMC] blob sn#031472 filedate 1973-03-25 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(This file is KNOW.NOT[226,JMC] and is being revised.)
C00017 00003	Hintikka, Jaako (1962) Knowledge and belief: an introduction
C00018 ENDMK
C⊗;
(This file is KNOW.NOT[226,JMC] and is being revised.)


SOME FORMALISM FOR KNOWLEDGE AND BELIEF

by John McCarthy


	Here are some formalisms that we propose to use to treat knowledge.
The approach is somewhat different from that of (McCarthy and Hayes 1969),
but the result formalism of that paper is used and some of the problems
treated are the same.
We shall deal with a certain class of symbolic expressions not yet determined
but which will contain expressions like

	telephone-number(Mike)

or in LISP notation

	(TELEPHONE-NUMBER MIKE).

In these notes, we shall often use an informal notation, but we expect
to use LISP S-expressions as the internal notation of some actual proof
checker or reasoning program.

	We are interested in expressions that have values and

	value[(TELEPHONE-NUMBER MIKE)]

denotes the value of (TELEPHONE-NUMBER MIKE).  
A reflection principle will be assumed to exist in the logic that will
generate assertions like

	value[(TELEPHONE-NUMBER MIKE)] = telephone-number(Mike).

	Such a reflection principle is like those in metamathematics that
generate assertions like

	true["It is snowing"] ≡ It is snowing,

but our form is more general and the greater generality seems to be required
for the applications.

	We may later have to give value two arguments, the second being an
environment or possible world or situation or something like that but for
the time being we will not do this.

	We will treat knowledge and belief by introducing 
value(<person>,<expression>,<situation>) where value(p,e,s) is the
value that p ascribes to e in s.  Thus

	value[John,(TELEPHONE-NUMBER MIKE),S0]

is the value that John ascribes to Mike's telephone number in situation S0.
Note that the situation argument refers to the situation in which the
ascription occurs not some situation referred to in the expression.

	With this notation we can say that John believs Mikes telephone number
is 321-1234 by writing

	value[John,(TELEPHONE-NUMBER MIKE),S0] = "321-1234"

where the number in quotes might have to be written
(3 2 1 - 1 2 3 4) in an actual LISP implementation.

	We can say that John knows Mike's telephone number without asserting
what this telephone number is by writing

	value[John,(TELEPHONE-NUMBER MIKE),S0] = telephone-number[Mike]

or

	value[John,(TELEPHONE-NUMBER MIKE),S0] = value[(TELEPHONE-NUMBER MIKE)].

These two sentences are equivalent by the reflection principle, and one
might therefore suppose that the value notation is superfluous.  Its
necessity arises as soon as we want to introduce quantifiers.

	Namely, we define knowing by the axiom

	(∀ p e s)(knows(p,e,s) ≡ value(p,e,s) = value(e),

and without the function value we couldn't write this definition.

	Now suppose we want to assert that the act of looking up someone's number
in the book results in one's knowing the number.  We first introduce the
notion of name as a function applied to people.  Naturally, we have

	name[Mike] = MIKE

where we shall regard MIKE as a LISP atom although we may later have to switch
to a notation in which it is a string of characters.  Our idea is that looking
up is an action performed on names and not on people.  We also have to use
the LISP function subst[x,y,z] which denotes the result of substituting the
expression x for each occurrence  of the expression y in the expression z.

	Now we write

	(∀ p q s)(value[p,subst[name[q],Q,(TELEPHONE-NUMBER Q)],
			result[p,lookup[name[q]],s]]
	= telephone-number[q]).

We could write simply (TELEPHONE-NUMBER name[q]) instead of "subst[...] provided
we understand that (TELEPHONE-NUMBER name[q]) stands for the result of
making a list out of TELEPHONE-NUMBER and whatever name[q] turns out to
be in the particular case.  In our scheme of things, to write
(TELEPHONE-NUMBER q) would be incorrect because this would be trying to put
a person into an S-expression where we can only put the name of a person.

	
Remarks:

	1. Tentatively, we shall treat only cases where the value of the
expressions considered is undefined or a symbolic expression or a number.
This is to avoid having to worry about "Mike knows John" wherein
value[Mike,denotation[JOHN],s] would have to be a person, and this seems
difficult to treat.

	2. The language in which the expressions are written is not
necessarily that of the person to whom values are being ascribed.  Thus
we want to say , value[Mikhail,(TELEPHONE-NUMBER ANDREI),S] = 65-03-52
without assuming that Mikhail speaks English or LISP.  Indeed, we
may want to say

	value[Fido,"hand with ball",S] = LEFT

in order to assert that Fido thinks the ball is in the left hand
without assuming that Fido uses language.  Naturally, in this
case we need to be especially careful about what we allow
ourselves to deduce from the assertion about what Fido believes.

	3. Metamathematical work concerning knowledge and belief has
mainly concerned knowledge of propositions.  Expressing this in terms
of knowledge and belief of sentences, i.e. symbolic expressions
representing the propositions, is one of the options that has been
considered.  The more popular option is to regard knowledge or belief
as a modal operator, because they resemble the operators of modal logic
in some of their properties.  I don't know any work in mathematical
logic that follows the same line as this paper in letting the operand
of belief be a general expression.

	Kaplan and Montague (1960) and Montague (1963) discuss
axiomatizations of knowledge and derive contradictions from a set
of very plausible axioms.  We intend to avoid these contradictions
by restricting what expressions can be operands of the value function,
we don't yet know what restrictions to impose.

	4. Most logicians and philosophers who have considered the matter
seem to believe that modal logic is the appropriate formalism for
expressing facts about knowledge and belief.  It seems to me that the
arguments presume that at most one of the proposed formalisms is right.
It seems evident to me, however, that whatever may be most convenient
in some general sense, making the object of belief an expression is an
option.  Namely, there is some relation between Fido and "the hand
holding the ball", and we are at liberty to study it if we want to.

	My opinion that this formalism will work out best for AI purposes,
however, is admittedly just a bet.  It is just that I wish to
avoid accusations that I don't understand the true nature of knowledge
just because I choose to study this relation rather than some other.


LOGIC OF BELIEF AND KNOWLEDGE

	Opportunities and difficulties arise when we attempt to deduce
from assertions that a person believes one thing to an assertion that
he believes something else.  These arise both from the practical AI
point of view and from the logical point of view.  Let's begin with
the AI point of view.

	Suppose I tell you that Smith is in New York.  Then I expect
you to know that Smith is not in California.  Therefore, our intuitive
notion of knowledge and belief expects certain consequences of things
believed also to be believed.  However, I obviously can't expect you
to believe all consequences of your beliefs.  A robot that
has to determine what people will do in response to what it tells
them will also have to reason from beliefs to beliefs.  Pending the
develpment of a notion of "obvious consequence", it may be best to
use axioms in which all consequences of beliefs are believed.

	Montague and Kaplan (1960) discuss the following axiom
schemes for knowledge of sentences:

	S1. K[p'] ⊃ p

	S2. K[[K[p'] ⊃ p]']

	S3. [I[p',q'] ∧ K[p']] ⊃ K[q'].

Here p and q are sentences and p' denotes the written form of p.  Thus
S1 asserts that if something is known, it is so, S2 asserts that this
principle is known, and S3 asserts that if q is deducible from p and p
is known, then q is known.

	They show that if a first order language contains elementary syntax
and all instances of these schemata, then it is inconsistent.  Montague (1963)
discusses these matters further.

	We plan to get out of the difficulty by putting some restriction on
the kind of sentences that can be known or believed.  These restrictions
will involve the way the knowledge operator and quantifiers can occur, but
I don't have a proposal yet.  Actually, the axioms and the restrictions will
take a different form, because we need the value[p,e,s] formalism, but all
the difficulties noted by Kaplan and Montague will arise, because the value
formalism includes theirs.

	A natural first axiom to consider in the "value" formalism is

	value[p,(f x),s] = value[p,f,x][value[p,x,s]].

This asserts that the value p gives for f(x) is the value he gives for f
applied to the value he gives for x.

	As stated, it seems that the principle is incorrect, because
a person could have a value for f(x) without having a value for f
or a value for x.  Therefore, we should rewrite it as

	value[p,f,s] ≠ UU ∧ value[p,x,s] ≠ UU
			⊃
	value[p,(f x),s] = value[p,f,x][value[p,x,s]].

	This could be criticised on the grounds that we should distinguish
between a person not having a value for an expression and his belief that
its value is undefined.  We shall have to revise this.

	Another issue is whether having a value for f(x) for all x implies
that one has a value for f.  Probably not.

Hintikka, Jaako (1962) Knowledge and belief: an introduction
to the logic of the two notions. New York: Cornell University
Press.

Kaplan, David and Montague, Richard (1960).  A paradox regained.
Notre Dame Journal of Formal Logic, vol. 1, pp. 79-90.

McCarthy, John and Hayes, Patrick (1969).  Some philosophical
problems from the standpoint of artificial intelligence.  in
Machine Intelligence 4, Edinburgh University Press, pp. 463-502.

Montague, Richard (1963). Syntactical treatments of Modality, with
corollaries on reflexion principles and finite axiomatizability.
Acta Philosophica Fennica, vol.  , pp. 153-167.